1. Field of the Invention
This invention relates generally to the field of functional verification of digital designs with respect to a set of requirements, and specifically to the formal verification of designs that have one or more datapaths.
2. Background of the Invention
Over the last 30 years, the complexity of integrated circuits has increased greatly. This increase in complexity has exacerbated the difficulty of verifying circuit designs. In a typical integrated circuit design process, which includes many steps, the verification step consumes approximately 70–80% of the total time and resources. Aspects of the circuit design such as time-to-market and profit margin greatly depend on the verification step. As a result, flaws in the design that are not found during the verification step can have significant economic impact by increasing time-to-market and reducing profit margins. To maximize profit, therefore, the techniques used for verification should be as efficient as possible.
As the complexity in circuit design has increased, there has been a corresponding improvement in various kinds of verification and debugging techniques. In fact, these verification and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among the combinational logic between registers.
Existing verification and debugging tools are used in the design flow of a circuit. The design flow begins with the creation of a circuit design at the RTL level using RTL source code. The RTL source code is specified according to a Hardware Description Language (HDL), such as Verilog HDL or VHDL. Circuit designers use high-level hardware description languages because of the size and complexity of modern integrated circuits. Circuit designs are developed in a high-level language using computer-implemented software applications, which enable a user to use text-editing and graphical design tools to create a HDL-based design.
In the design flow, creation of the RTL source code is followed by verification of the design to check if the RTL source code meets various design specifications. This verification is performed by simulation of the RTL code using a “testbench,” which includes stimulus generators and requirement monitors. The verification method involving the use of RTL source code and testbench is referred to as the simulation process. For a circuit having n inputs, there would be 2n possible combinations of inputs at any given time. Where n is large, such as for a complex design, the number of possible input sequences becomes prohibitively large for verification. To simplify the verification process, therefore, only a subset of all possible inputs is described in a particular testbench.
The increasing complexity of circuit designs has lead to several drawbacks associated with simulation-based techniques. Reasons for these drawbacks include the requirement of a large amount of time to verify circuit designs, the use of a large amount of resources and thus large costs, and the inability to verify large designs completely and quickly. For large and complex designs in which many combinations of inputs are possible, therefore, the simulation process is not reliable. This is because the simulation process verifies the circuit only for a subset of inputs described in the testbench; thus, circuit behavior for all possible combinations of inputs is not checked.
An increasingly popular alternative is to use formal methods to verify the properties of a design completely. Formal methods use mathematical techniques to prove that a design property is either always true or to provide an example condition (called a counterexample) that demonstrates the property is false. Tools that use formal methods to verify RTL source code and design properties are known as “model checkers.” Design properties to be verified include specifications and/or requirements that must be satisfied by the circuit design. Since mathematical properties define the design requirements in pure mathematical terms, this enables analysis of all possible valid inputs for a given circuit and is akin to an exhaustive simulation. Formal verification methods are therefore more exhaustive when compared to simulation methods. Moreover, formal verification methods provide many advantages over the simulation methods, such as reduced validation time, quicker time-to-market, reduced costs, and high reliability.
Performance limits and resource availability inhibit the widespread use of model checking. The resources required to perform verification are typically exponentially related to the number of registers in the circuit model, as well as other characteristics. This is referred to as the “state space explosion” problem. Many conventional model checkers analyze the entire design before proving a particular property, verifying the behavior of the design with all possible inputs at all times. These model checking techniques thus rely on an underlying reachability analysis and must iterate through time to collect all possible states into a data structure. But the complexity and size of modern integrated circuits, combined with the state space explosion problem, make it impossible to use conventional model checkers on complex designs.
Moreover, functional formal verification tools often encounter capability limitations, which in many cases are due to the need to process an increased state-space encountered by circuit designs that contain datapaths. Today, digital designs commonly include a combination of control logic and datapath circuits. Functional formal verification schemes using theorem proving, model checking, or other techniques are limited in their ability to verify designs that contain datapath circuits. Therefore, the successful application of functional formal verification on designs that contain datapath logic has historically required significant manual abstraction of the datapath circuits in the design. A process of applying manual abstractions to circuit designs with datapaths typically includes: (1) manually inspecting the design architecture to discover possible datapath abstractions; (2) manually altering the original design model to include an abstract model of the datapath circuit; and (3) performing functional formal verification on the abstract model. These manual abstractions are typically performed by an expert with significant background in formal verification and abstraction techniques, which are not well understood by designer or verification engineers. Specific techniques have been proposed to automate a portion of this abstraction process, but functional formal verification of designs that contain datapath logic in an industrial setting has not reached mainstream acceptance because of the limitations of these techniques. Accordingly, a need remains for simplifying the verification of designs that have datapaths without having the limitations of existing formal verification methods.